;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "mgreyscale.lisp")
(require "mbmptree.lisp")
(require "mavltree.lisp")
(require "mdatagenerators.lisp")

(module tGreyscale
  (import iGreyscale)
  (import iBmptree)
  (import iAvltree)
  (import iDataGenerators)
  (include-book "testing" :dir :teachpacks)
  (include-book "doublecheck" :dir :teachpacks) 
  (include-book "io-utilities" :dir :teachpacks)
  (include-book "list-utilities" :dir :teachpacks)
  
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ; DATA GENERATORS
  ; Generates a random pixel (random RGB values).
  (defrandom random-pixel ()
    (let* ((r (random-between 0 255))
           (g (random-between 0 255))
           (b (random-between 0 255)))
      (list r g b)))
 
  ; Random bitmap file, uses a static header with a 
  ; size of heightxwidth.
  (defrandom random-bitmap (height width)
    (let* ((header (list 66 77 54 12 0 0 0 0 0 0 54 0 0 
                         0 40 0 0 0 width 0 0 0 height 0 0 0 1 
                         0 24 0 0 0 0 0 0 12 0 0 0 0 0 
                         0 0 0 0 0 0 0 0 0 0 0 0 0))
           (pixels (random-list-of (random-pixel) :size (* width height)))
           (tr (insert-header (empty-bmp-tree) header)))
      (fill-bitmap tr 0 0 height width pixels)))
  
  
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ; SANITY CHECKS
  (check-expect (pixel-to-greyscale 0 0 0 0) (list 0 0 0 0))
  (check-expect (pixel-to-greyscale 0 256 0 0) "Invalid RGB value.")
  (check-expect (pixel-to-greyscale 0 100 70 0) (list 0 50 50 50))
  (check-expect (pixel-to-greyscale 0 255 255 255) (list 0 255 255 255))
  
  (check-expect (make-greyscale-columns nil nil) nil)
  
  (check-expect (greyscale (make-bmp-tree 
                             (list (list 0 0 0 0 0 0 0 0 0 0 0 0
                                         0 0 0 0 0 0 3 0 0 0 3)
                                   (list 0 0 (list 40 10 90)) 
                                   (list 0 1 (list 10 30 40))
                                   (list 0 2 (list 90 40 55)) 
                                   (list 1 0 (list 30 76 90))
                                   (list 1 1 (list 255 255 255)) 
                                   (list 1 2 (list 0 0 0))
                                   (list 2 0 (list 200 40 150)) 
                                   (list 2 1 (list 8 8 8))
                                   (list 2 2 (list 9 9 9)))))
                (make-bmp-tree 
                 (list (list 0 0 0 0 0 0 0 0 0 0 0 0
                             0 0 0 0 0 0 3 0 0 0 3)
                       (list 0 0 (list 50 50 50)) 
                       (list 0 1 (list 25 25 25))
                       (list 0 2 (list 65 65 65)) 
                       (list 1 0 (list 60 60 60))
                       (list 1 1 (list 255 255 255)) 
                       (list 1 2 (list 0 0 0))
                       (list 2 0 (list 120 120 120)) 
                       (list 2 1 (list 8 8 8))
                       (list 2 2 (list 9 9 9)))))
  
  
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ; PROPERTIES
  ; pixel-to-greyscale returns a list of 4 numbers,
  ; with the first number being the given column number
  ; and the last three being values between [0, 255]
  (defproperty pixel-to-greyscale-returns-list-of-4-prp
    (r   :value (random-natural)
         :where (<= r 255)
     g   :value (random-natural)
         :where (<= g 255)
     b   :value (random-natural)
         :where (<= b 255)
     col :value (random-natural))
    (let* ((newRGB (pixel-to-greyscale col r g b))
           (newR   (cadr newRGB))
           (newG   (caddr newRGB))
           (newB   (cadddr newRGB)))
      (and (= (len newRGB) 4)
           (and (natp newR) (<= newR 255))
           (and (natp newG) (<= newG 255))
           (and (natp newB) (<= newB 255)))))
  
  ; pixel-to-greyscale always returns a grey value,
  ; meaning r = g = b.
  (defproperty pixel-to-greyscale-returns-grey-prp
    (r   :value (random-natural)
         :where (<= r 255)
     g   :value (random-natural)
         :where (<= g 255)
     b   :value (random-natural)
         :where (<= b 255)
     col :value (random-natural))
    (let* ((grey (pixel-to-greyscale col r g b))
           (newR (cadr grey))
           (newG (caddr grey))
           (newB (cadddr grey)))
    (and (equal newR newG)
         (equal newG newB))))
  
  ; If pixel is already grey, pixel-to-greyscale returns
  ; the original values.
  (defproperty pixel-to-greyscale-already-grey-prp
    (grey :value (random-natural)
          :where (<= grey 255)
     col  :value (random-natural))
    (equal (pixel-to-greyscale col grey grey grey) (list col grey grey grey)))
  
  ; make-greyscale-columns returns a list of the correct length
  (defproperty make-greyscale-columns-returns-correct-number-of-columns-prp
    (ht  :value (random-between 1 25)
     wd  :value (random-between 1 25)
     tr  :value (random-bitmap ht wd)
     ndx :value (random-between 0 (- ht 1))
     row :value (get-row tr ndx))
    (= (length (make-greyscale-columns row nil)) wd))
  
  ; make-greyscale-columns returns a list
  (defproperty make-greyscale-columns-returns-list-prp
    (ht  :value (random-between 1 25)
     wd  :value (random-between 1 25)
     tr  :value (random-bitmap ht wd)
     ndx :value (random-between 0 (- ht 1))
     row :value (get-row tr ndx))
    (listp (make-greyscale-columns row nil)))
  
  ; The greyscale function always returns a bitmap tree.
  (defproperty greyscale-returns-tree-prp
    (ht :value (random-between 1 25)
     wd :value (random-between 1 25)
     tr :value (random-bitmap ht wd))
    (bmp-tree? (greyscale tr))))
  
(link rtGreyscale (mAvlTree mBmpTree mDataGenerators mGreyscale tGreyscale))
(invoke rtGreyscale)